f-msg{$wanted:ut2, $free:ut2, $z:ut2}
f-msg(es; L; e)
== (loc(e)  L)
==  ((es-isrcv(es; e))
==  c (((es-tag(es; e) = mkid{$wanted:ut2})  (es-tag(es; e) = mkid{$free:ut2}))
==  c  (i:Id. ((i  L)  ((i = loc(e)))  (es-lnk(es; e) = <i, loc(e), mkid{$z:ut2}>))))) 

latex

---

clarification:

f-msg{$wanted:ut2, $free:ut2, $z:ut2}
f-msg(es; L; e)
== (es-loc(es; e)  L  Id)
==  ((es-isrcv(es; e))
==  c (((es-tag(es; e) = mkid{$wanted:ut2}  Id)  (es-tag(es; e) = mkid{$free:ut2}  Id))
==  c  (i:Id
==  c  (((i  L  Id)
==  c  ( ((i = es-loc(es; e)  Id))
==  c  ( (es-lnk(es; e) = <i, es-loc(es; e), mkid{$z:ut2}>  IdLnk))))) 

latex

Definitions	A c B, b, es-isrcv(es; e), P  Q, es-tag(es; e), x:A. B(x), (x  l), P  Q, A, Id, s = t, IdLnk, es-lnk(es; e), <a, b>, loc(e), mkid{$x:ut2}
FDL editor aliases	f-msg